Separation Logic

In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs.
It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI). A CACM review article by O'Hearn charts developments in the subject to early 2019.

Overview

Separation logic facilitates reasoning about:

* programs that manipulate pointer data structures—including information hiding in the presence of pointers;
* ''"transfer of ownership"'' (avoidance of semantic frame axioms); and
* virtual separation (modular reasoning) between concurrent modules.

Separation logic supports the developing field of research described by Peter O'Hearn and others as ''local reasoning'', whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification (where an algorithm checks the validity of another algorithm) and automated parallelization of software.

Assertions: operators and semantics

Separation logic assertions describe "states" consisting of a ''store'' and a ''heap'', roughly corresponding to the state of local (or ''stack-allocated'') variables and ''dynamically-allocated'' objects in common programming languages such as C and Java. A store $s$ is a function mapping variables to values. A heap $h$ is a partial function mapping memory addresses to values. Two heaps $h$ and $h'$ are ''disjoint'' (denoted $h \,\bot\, h'$) if their domains do not overlap (i.e., for every memory address $\ell$, at least one of $h(\ell)$ and $h'(\ell)$ is undefined).

The logic allows to prove judgements of the form $s, h \models P$, where $s$ is a store, $h$ is a heap, and $P$ is an ''assertion'' over the given store and heap. Separation logic assertions (denoted as $P$, $Q$, $R$) contain the standard boolean connectives and, in addition, $\mathbf\mathbf\mathbf$, $e \mapsto e'$, $P \ast Q$, and $P \, Q$, where $e$ and $e'$ are expressions.
* The constant $\mathbf\mathbf\mathbf$ asserts that the heap is ''empty'', i.e., $s, h \models \mathbf\mathbf\mathbf$ when $h$ is undefined for all addresses.
* The binary operator $\mapsto$ takes an address and a value and asserts that the heap is defined at exactly one location, mapping the given address to the given value. I.e., $s, h \models e \mapsto e'$ when h( ![e!.html"_;"title=".html"_;"title="![e">![e!">.html"_;"title="![e">![e!)_=_[\![e'.html" ;"title="">![e!.html" ;"title=".html" ;"title="![e">![e!">.html" ;"title="![e">![e!) = [\![e'">">![e!.html" ;"title=".html" ;"title="![e">![e!">.html" ;"title="![e">![e!) = [\![e'!]_ (where ![e!.html" ;"title=".html" ;"title="![e">![e!">.html" ;"title="!![e!_denotes_the_value_of_expression_$e$_evaluated_in_store_$s$)_and_$h$_is_otherwise_undefined.
*_The_binary_operator_$\ast$_(pronounced_''star''_or_''separating_conjunction'')_asserts_that_the_heap_can_be_split_into_two_''disjoint''_parts_where_its_two_arguments_hold,_respectively._I.e.,_$s,_h_\models_P_\ast_Q$_when_there_exist_$h_1,_h_2$_such_that_$h_1_\,\bot\,_h_2$_and_$h_=_h_1_\cup_h_2$_and_$s,_h_1_\models_P$_and_$s,_h_2_\models_Q$.
*_The_binary_operator_$-\!\!\ast$_(pronounced_''magic_wand''_or_''separating_implication'')_asserts_that_extending_the_heap_with_a_disjoint_part_that_satisfies_its_first_argument_results_in_a_heap_that_satisfies_its_second_argument._I.e,._$s,_h_\models_P_-\!\!\ast\,_Q$_when_for_every_heap_$h'_\,\bot\,_h$_such_that_$s,_h'_\models_P$,_also_$s,_h_\cup_h'_\models_Q$_holds.

The_operators_$\ast$_and_$-\!\!\ast$_share_some_properties_with_the_classical_ ![e!_denotes_the_value_of_expression_$e$_evaluated_in_store_$s$)_and_$h$_is_otherwise_undefined.
*_The_binary_operator_$\ast$_(pronounced_''star''_or_''separating_conjunction'')_asserts_that_the_heap_can_be_split_into_two_''disjoint''_parts_where_its_two_arguments_hold,_respectively._I.e.,_$s,_h_\models_P_\ast_Q$_when_there_exist_$h_1,_h_2$_such_that_$h_1_\,\bot\,_h_2$_and_$h_=_h_1_\cup_h_2$_and_$s,_h_1_\models_P$_and_$s,_h_2_\models_Q$.
*_The_binary_operator_$-\!\!\ast$_(pronounced_''magic_wand''_or_''separating_implication'')_asserts_that_extending_the_heap_with_a_disjoint_part_that_satisfies_its_first_argument_results_in_a_heap_that_satisfies_its_second_argument._I.e,._$s,_h_\models_P_-\!\!\ast\,_Q$_when_for_every_heap_$h'_\,\bot\,_h$_such_that_$s,_h'_\models_P$,_also_$s,_h_\cup_h'_\models_Q$_holds.

The_operators_$\ast$_and_$-\!\!\ast$_share_some_properties_with_the_classical_Logical_Conjunction">conjunction_

Conjunction_may_refer_to:
*_Conjunction_(grammar),_a_part_of_speech
*_Logical_conjunction,_a_mathematical_operator
**_Conjunction_introduction,_a_rule_of_inference_of_propositional_logic
*_Conjunction_(astronomy),_in_which_two_astronomical_bodies__...
_and_Entailment.html" ;"title="Logical_Conjunction.html" "title="">![e! denotes the value of expression $e$ evaluated in store $s$) and $h$ is otherwise undefined.
* The binary operator $\ast$ (pronounced ''star'' or ''separating conjunction'') asserts that the heap can be split into two ''disjoint'' parts where its two arguments hold, respectively. I.e., $s, h \models P \ast Q$ when there exist $h_1, h_2$ such that $h_1 \,\bot\, h_2$ and $h = h_1 \cup h_2$ and $s, h_1 \models P$ and $s, h_2 \models Q$.
* The binary operator $-\!\!\ast$ (pronounced ''magic wand'' or ''separating implication'') asserts that extending the heap with a disjoint part that satisfies its first argument results in a heap that satisfies its second argument. I.e,. $s, h \models P -\!\!\ast\, Q$ when for every heap $h' \,\bot\, h$ such that $s, h' \models P$, also $s, h \cup h' \models Q$ holds.

The operators $\ast$ and $-\!\!\ast$ share some properties with the classical Logical Conjunction">conjunction